(set-option :model_validate true)
(declare-const v12 Bool)
(declare-const v33 Bool)
(assert (= true true true v12 v33))
(check-sat-using (then simplify reduce-invertible horn))